A:Type, eq:EqDecider(A), B:(AType), L:(a:A fp B(a) List), x:A.
(x  dom((L)))  (fL.x  dom(f)) 

latex

Definitions	t  T, f(a), x(s), x. t(x), x:A. B(x), a:A fp B(a), type List, x:AB(x), b, (xL.P(x)), P  Q, Type, EqDecider(T), False, P  Q, P  Q, P & Q, x.A(x), x  dom(f), , Top, [], x:A  B(x), (L), left + right, P  Q, S  T, [car / cdr], (x  l), {T}, if b then t else f fi
Lemmas	fpf-join-dom, l exists cons, top wf, fpf-join-list wf, all functionality wrt iff, iff functionality wrt iff, l exists nil, fpf-trivial-subtype-top, iff wf, l exists wf, assert wf, fpf-dom wf, false wf, deq wf, fpf wf